E:Type, V:(KndIdType), info:(E(IdId+(IdLnkE)Id)), val:(e:EV(kind(e),loc(e))), e:E.
rcv?(e)  rmsg(info;val;e)  Msg(l,tg. V(rcv(l,tg),destination(l))) 

latex

Definitions	kind(e), loc(e), Msg(M), Knd, rmsg(info;val;e), rcv?(e), link(e), rtag(info;e), ecase1(e;info;i.f(i);l,e'.g(l;e')), b, False, locl(a), P  Q, msg(l;t;v), IdLnk, Id, True, rcv(l,tg), t  T, destination(l), x:A. B(x)
Lemmas	ldst wf, rcv wf, true wf, msg wf, locl wf, false wf, IdLnk wf, loc wf, kind wf, Id wf, Knd wf, rcv? wf, assert wf